(setf (symbol-function 'is-variable) 
  #'(lambda(x)(symbolp x)))

(setf (symbol-function 'is-function) 
  #'(lambda(L)(and (listp L)
                     (= (first L) '^)
                     (= (nth 2 L) '=>))))

(setf (symbol-function'function-variable)
 #'(lambda(f)(nth 1 f)))

(setf (symbol-function 'function-body)
 #'(lambda(f)(last f)))
                                 
(setf (symbol-function 'is-application)
 #'(lambda(L)(and (listp L)
              (= (length L) 2))))
                                 
(setf (symbol-function 'substitute-free-occurences) ; of variable V in E with F
     #'(lambda(V E F)
     
       (cond ((is-variable E) (if (= E V) F E))

             ((is-function E)
             
                  (if (= (function-variable E) V)
                      
                      E ; V is bounded in E - no substitution
                      
                      (list '^
                            (function-variable E)
                            '=>
                            (substitute-free-occurences V
                                   (function-body E)
                                   F))))
                        
              ((is-application E)
               (list (substitute-free-occurences V (first E) F)
                     (substitute-free-occurences V (last E) F))))))

(setf (symbol-function 'reduce-once-our)
     #'(lambda(E)
        (cond ((is-variable E) E)
              ((is-function E) E)      
              ((is-application E)
                (let ((E1 (first E))
                      (E2 (last E)))
                
                (if (is-function E1)
                   

                    (substitute-free-occurences (function-variable E1)
                                                (function-body E1)
                                                E2)
                     
                     (let ((new-E1 (reduce-once-our E1)))

                           (if (!= new-E1 E1)
                               (list new-E1 E2)
                               (list E1 (reduce-once-our E2))))))))))


(setf (symbol-function 'reduce-our)
        #'(lambda(new-expression)
                (setf expression nil)
                  (format t "~%--------------~% ~% ~A" (string new-expression))
                  (format t "~%--------------~% ~% ~A" (string expression))
                  (loop while (not (string-equal (string new-expression) (string expression))) do
                            (setf expression new-expression)
                            (setf new-expression (reduce-once-our expression))
                            (if (not (string-equal (string new-expression) (string expression)))
                                (format t " ==> ~A Further reductions are impossible.~%"
                                 (string new-expression))
                new-expression))))



(defun sample (root)
  (dolist (i '( x
             ('^ 'x '=> 'x)
             ((^ x => x) y)
             ((^ x => a) ((^ y => y) z))  
             ((^ y => (^ z => z)) ((^ x => (x x)) (^ v => (v v))))
             ((((^ v => (^ t => (^ f => ((v t) f)))) (^ x => (^ y => x))) a) b)
             ((((^ v => (^ t => (^ f => ((v t) f)))) (^ x => (^ y => y))) a) b)
             ((^ x .=> (x x)) (^ x => (x x)))
             ))
   
   (reduce-our i)))